$\forall$$T$:Type, $L$:($T$ List), $x$:$T$. ($x$ $\in$ $L$) $\Rightarrow$ ($\neg$($x$ = last($L$))) $\Rightarrow$ $x$ before last($L$) $\in$ $L$